Nuprl Lemma : bool-tt-or-ff
11,40
postcript
pdf
b
:
. (
b
= tt)
(
b
= ff)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
left
+
right
,
s
=
t
,
,
Unit
,
P
Q
,
P
&
Q
,
x
:
A
B
(
x
)
,
A
,
P
Q
,
x
:
A
B
(
x
)
,
b
,
{
T
}
,
ff
,
t
T
,
Lemmas
bfalse
wf
,
assert
of
bnot
,
eqff
to
assert
,
iff
transitivity
,
eqtt
to
assert
origin
b:
. (b = tt) 
(b = ff) b:. (b = tt) (b = ff) x:A. B(x) Q
Q
B(x)
A Q
B(x)
b
T